perm filename NTH[EKL,SYS]4 blob
sn#824859 filedate 1986-09-25 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00018 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00003 00002 facts about nth, nthcdr and fstposition
C00005 00003 forms of doubleinduction
C00013 00004 basic facts about nth
C00023 00005 nthcdr
C00026 00006 fstposition
C00028 00007 injectivity
C00029 00008 miscellaneous facts: nth, allp and mklset
C00030 00009 * forms of doubleinduction
C00050 00010 basic facts about nth
C00052 00011 member_nth
C00054 00012 proofs of other facts needed verification of facts about nthcdr
C00070 00013 nthcdr_induction1 and nthcdr_induction
C00079 00014 facts about fstposition
C00084 00015 lemmata nth_fstposition and fstposition_nth
C00086 00016 equivalence of uniqueness and inj
C00089 00017 equivalence of uniqueness and inj
C00092 00018 proof of facts about sets
C00094 ENDMK
C⊗;
;facts about nth, nthcdr and fstposition
(wipe-out)
(get-proofs length prf ekl sys)
(proof lispax)
;now we need to tie up natural numbers and s-expressions
(axiom |∀n.urelement n|)
(label simpinfo)
(axiom |∀n.sexp n|)
(label simpinfo)
(axiom |∀n.¬null(n)|)
(label simpinfo)
;forms of doubleinduction
(proof listinduction)
;a convenient form for double induction on lists
(axiom |∀phi2.(∀u v x y.phi2(nil,u)∧phi2(u,nil)∧(phi2(u,v)⊃phi2(x.u,y.v)))⊃(∀u v.phi2(u,v))|)
(label doubleinduction)
;the next principle gives a form of double induction for lists and numbers
(axiom |∀phi3.(∀u n x.phi3(nil,n)∧phi3(u,0)∧(phi3(u,n)⊃phi3(x.u,n')))⊃(∀u n.phi3(u,n))|)
(label doubleinduction1)
;basic facts about nth
(proof nth)
;1
(decl nth (syntype: constant) (type: |ground⊗ground→ground|))
;2
(defax nth |∀x u n.nth(nil,n)=nil∧nth(u,0)=car u∧
nth(x.u,n')=nth(u,n)|)
(label simpinfo) (label nthdef)
;well-definedness of nth
;3
(axiom |∀u n.sexp nth(u,n)|)
(label simpinfo)(label sexp_nth)
;membership of nth in the original list
;4
(axiom |∀u n.n<length u⊃member(nth(u,n),u)|)
(label nthmember)
;we need a converse of nthmember
;5
(axiom |∀u y.member(y,u)⊃(∃n.n<length u∧nth(u,n)=y)|)
(label member_nth)
;nthcdr
(proof nthcdr)
;1
(decl nthcdr (syntype: constant) (type: |ground⊗ground→ground|))
;2
(defax nthcdr |∀x u n.nthcdr(nil,n)=nil∧nthcdr(u,0)=u∧
nthcdr(x.u,n')=nthcdr(u,n)|)
(label simpinfo) (label nthcdrdef)
;3
(axiom |∀u n.listp nthcdr(u,n)|)
(label simpinfo)
;4
;nth nthcdr zero
(axiom |∀u.0<length u⊃nth(u,0).nthcdr(u,1)=u|)
(label nth_nthcdr_zero)
;5
;car nthcdr
(axiom |∀u n.n<length u⊃car nthcdr(u,n)=nth(u,n)|)
(label car_nthcdr)
;6
;cdr nthcdr
(axiom |∀u n.cdr nthcdr(u,n)=nthcdr(u,n')|)
(label cdr_nthcdr)
;7
;nthcdr car cdr
(axiom |∀u n.n<length u⊃nthcdr(u,n)=nth(u,n).nthcdr(u,n')|)
(label nthcdr_car_cdr)
;8
;nth in nthcdr
(axiom |∀u n m.n≤m∧m<length u⊃member(nth(u,m),nthcdr(u,n))|)
(label nth_in_nthcdr)
;9
;nth nthcdr
(axiom |∀u n m.n<length u∧m<length (nthcdr(u,n))⊃nth(nthcdr(u,n),m)=nth(u,m+n)|)
(label nth_nthcdr)
;10
;length nthcdr
(axiom |∀u n.n≤length u⊃length (nthcdr(u,n))=length u-n|)
(label length_nthcdr)
;11
(axiom |∀u.nthcdr(u,length u)=nil|)
(label last_nthcdr)
;12
(axiom |∀u n.length(u)≤n⊃nthcdr(u,n)=nil|)
(label trivial_nthcdr)
;13
(axiom |∀a u n.allp(a,u)⊃allp(a,nthcdr(u,n))|)
(label allp_nthcdr)
;local listinduction, using nth and nthcdr
;14
(axiom |∀phi4 u.phi4(nil,length u)∧
(∀n.n<length u∧phi4(nthcdr(u,n'),n')⊃phi4(nth(u,n).nthcdr(u,n'),n))⊃phi4(u,0)|)
(label nthcdr_induction1)
;15
(axiom |∀phi u.phi(nil)∧(∀n.n<length(u)⊃
(phi(nthcdr(u,n'))⊃phi(nth(u,n).nthcdr(u,n'))))⊃phi(u)|)
(label nthcdr_induction)
;fstposition
(proof fstposition)
(decl (fstposition) (type: |ground⊗ground→ground|))
(define fstposition |∀x u y.fstposition(nil,y)=nil∧
fstposition(x.u,y)=if ¬member(y,x.u) then nil else
if x=y then 0 else add1(fstposition(u,y))|
listinductiondef)
(label fstpositiondef)
(axiom |∀u y.(null fstposition(u,y)⊃¬member(y,u))∧
(member(y,u)⊃natnum(fstposition(u,y)))∧
(null fstposition(u,y)∨natnum(fstposition(u,y)))|)
(label simpinfo)(label posfacts)
(axiom |∀u y.sexp fstposition(u,y)|)
(label simpinfo)(label sortpos)
(axiom |∀u y.member(y,u)⊃fstposition(u,y)<length u|)
(label pos_length)
(axiom |∀u n.member(n,u)⊃nth(u,fstposition(u,n))=n|)
(label nth_fstposition)
(axiom |∀u n.uniqueness(u)∧member(n,u)⊃fstposition(u,nth(u,n))=n|)
(label fstposition_nth)
;injectivity
;another predicate for uniqueness
(proof inj)
(decl (inj) (type: |ground→truthval|))
(define inj |∀u.inj(u)=∀n m.n<length(u)∧m<length(u)∧nth(u,n)=nth(u,m)⊃n=m|)
(label injdef)
(axiom |∀u.uniqueness(u)≡inj(u)|)
(label uniqueness_injectivity)
;miscellaneous facts: nth, allp and mklset
(proof allp)
(axiom |∀phi1 u.(∀n.n<length u⊃phi1(nth(u,n)))⊃allp(phi1,u)|)
(label nth_allp)
(proof sets)
(axiom |∀u.mklset(u)=(λx.(∃k.k<length u∧nth(u,k)=x))|)
(label mklset_fact)
(save-proofs nth)
;* forms of doubleinduction
;time 9s
(wipe-out)
(get-proofs nth prf ekl sys)
(proof listinduction)
;a useful principle which follows from listinduction
;corresponds to a proof by cases arguments
(trw |∀phi.(phi(nil)∧∀x u.phi(x.u))⊃∀u.phi(u)| listinduction)
;∀PHI.PHI(NIL)∧(∀X U.PHI(X.U))⊃(∀U.PHI(U))
(label listcases)
;the next principle gives a convenient form for double induction on lists
(assume |∀u v x y.phi2(nil,u)∧phi2(u,nil)∧(phi2(u,v)⊃phi2(x.u,y.v))|)
(label dindass)
(ue (phi |λu.∀v.phi2(u,v)|) listinduction
(use dindass) (use listcases ue: ((phi.|λv.phi2(x.u,v)|)) ))
;∀U V.PHI2(U,V)
;deps: (DINDASS)
(ci (dindass) *)
;(∀U V X Y.PHI2(NIL,U)∧PHI2(U,NIL)∧(PHI2(U,V)⊃PHI2(X.U,Y.V)))⊃(∀U V.PHI2(U,V))
(label doubleinduction)
;the next principle gives a form of double induction for lists and numbers
(assume |∀u n x.phi3(nil,n)∧phi3(u,0)∧(phi3(u,n)⊃phi3(x.u,n'))|)
(label dindass1)
(ue (phi |λu.∀n.phi3(u,n)|) listinduction
(use dindass1) (use proof_by_induction ue: ((a.|λn.phi3(x.u,n)|)) ))
;∀U N.PHI3(U,N)
;deps: (DINDASS1)
(ci (dindass1) *)
;(∀U N X.PHI3(NIL,N)∧PHI3(U,0)∧(PHI3(U,N)⊃PHI3(X.U,N')))⊃(∀U N.PHI3(U,N))
(label doubleinduction1)
;basic facts about nth
;15s
(wipe-out)
(get-proofs nth prf ekl sys)
(proof nth)
;prove by double induction the well-definedness of nth for the obvious range
;3
(unlabel simpinfo sexp_nth)
(ue (phi3 |λu n.sexp nth(u,n)|) doubleinduction1 (open nth))
;∀U N.SEXP NTH(U,N)
(label simpinfo sexp_nth)
;4
;prove by double induction the membership of nth in the original list
(ue (phi |λu.0<length u⊃member(nth(u,0),u)|) listinduction
(open length nth member))
;∀U.0<LENGTH U⊃MEMBER(NTH(U,0),U)
(ue (phi3 |λu n.n<length u ⊃ member(nth(u,n),u)|) doubleinduction1
(open length nth) (use memberdef mode: always)(use *))
;∀U N.N<LENGTH U⊃MEMBER(NTH(U,N),U)
(label nthmember)
;member_nth
(wipe-out)
(get-proofs nth prf ekl sys)
(proof member_nth)
(assume |(member(y,u)⊃(∃n.n<length u∧nth(u,n)=y))|)
(label m_n1)
(assume |y=x|)
(label m_n2)
(trw |0<length(x.u)∧nth(x.u,0)=y| (open nth) *)
;0<LENGTH (X.U)∧NTH(X.U,0)=Y
(derive |∃n.n<length(x.u)∧nth(x.u,n)=y| *)
(label m_n3)
(assume |member(y,u)|)
(define nv |nv<length u∧nth(u,nv)=y| (m_n1 *))
(trw |nv'<length(x.u)∧nth(x.u,nv')=y| (open nth) * )
;NV'<LENGTH (X.U)∧NTH(X.U,NV')=Y
(derive |∃n.n<length(x.u)∧nth(x.u,n)=y| *)
(label m_n4)
(assume |member(y,x.u)| )
(label m_n5)
(rw * (open member))
;Y=X∨MEMBER(Y,U)
(cases * m_n3 m_n4)
;∃N.N<LENGTH (X.U)∧NTH(X.U,N)=Y
(ci m_n5)
;MEMBER(Y,X.U)⊃(∃N.N<LENGTH U'∧NTH(X.U,N)=Y)
(ci m_n1)
(ue (phi |λu.member(y,u)⊃(∃n.n<length u∧nth(u,n)=y)|) listinduction
(open member nth) *)
;∀U.MEMBER(Y,U)⊃(∃N.N<LENGTH U∧NTH(U,N)=Y)
(wipe-out)
(get-proofs sums prf ekl sys)
(ue (phi |(member(y,u)⊃some(length u,λn.n<length u∧nth(u,n)=y))|)
listinduction (open member some) (use normal mode: always))
;proofs of other facts needed; verification of facts about nthcdr
(wipe-out)
(get-proofs nth prf ekl sys)
(proof nthcdr)
;3
(unlabel simpinfo nthcdr#3)
(ue (phi3 |λu n.listp nthcdr(u,n)|) doubleinduction1
(open nthcdr) )
(label simpinfo nthcdr#3)
;∀U N.LISTP NTHCDR(U,N)
;4
;nth_nthcdr_zero
(ue (phi |λu.0<length u⊃nth(u,0).nthcdr(u,0')=u|) listinduction
(open length nth nthcdr))
;∀U.0<LENGTH U⊃NTH(U,0).NTHCDR(U,1)=U
;5
;car_nthcdr
(ue (phi3 |λu n.n<length(u)⊃car(nthcdr(u,n))=nth(u,n)|) doubleinduction1
(open length nthcdr nth))
;∀U N.N<LENGTH U⊃CAR NTHCDR(U,N)=NTH(U,N)
;7
;cdr_nthcdr
(ue (phi |λu.cdr(nthcdr(u,0))=nthcdr(u,0')|) listinduction
(open nthcdr))
;∀U.CDR U=NTHCDR(U,1)
(ue (phi3 |λu n.cdr(nthcdr(u,n))=nthcdr(u,n')|) doubleinduction1
(open nthcdr) *)
;∀U N.CDR NTHCDR(U,N)=NTHCDR(U,N')
;8
;nthcdr_car_cdr
(ue (phi |λu.0<length(u)⊃nthcdr(u,0)=nth(u,0).nthcdr(u,0')|) listinduction
( car_nthcdr cdr_nthcdr))
;∀U.0<LENGTH U⊃U=CAR U.NTHCDR(U,1)
(ue (phi3 |λu n.n<length(u)⊃nthcdr(u,n)=nth(u,n).nthcdr(u,n')|) doubleinduction1
(open length)(use car_nthcdr cdr_nthcdr) *)
;∀U N.N<LENGTH U⊃NTHCDR(U,N)=NTH(U,N).NTHCDR(U,N')
;10
;last_nthcdr
(ue (phi |λu.nthcdr(u,length(u))=nil|) listinduction
(open nthcdr))
;∀U.NTHCDR(U,LENGTH U)=NIL
;11
;nth in nthcdr
(assume |∀M.(N<M∧M<LENGTH U⊃MEMBER(NTH(U,M),NTHCDR(U,N)))|)
(label nincdr1)
(ue (a |λM.(N'<M∧M<LENGTH(X.U)⊃MEMBER(NTH(X.U,M),NTHCDR(X.U,N')))|) proof_by_induction
(part 2(nuse nthdef nthcdrdef lengthdef)) nincdr1 zero_non_less_successor)
;∀N2.N'<N2∧N2<LENGTH (X.U)⊃MEMBER(NTH(X.U,N2),NTHCDR(X.U,N'))
(ci NINCDR1)
;(∀M.N<M∧M<LENGTH U⊃MEMBER(NTH(U,M),NTHCDR(U,N)))⊃
;(∀N2.N'<N2∧N2<LENGTH U'⊃MEMBER(NTH(X.U,N2),NTHCDR(U,N)))
(ue (phi3 |λu n.∀m.n<m∧m<length(u)⊃member(nth(u,m),nthcdr(u,n))|) doubleinduction1
(use nthmember mode: exact) (use * mode: exact))
;(∀U N M.N<M∧M<LENGTH U⊃MEMBER(NTH(U,M),NTHCDR(U,N)))
(trw |∀u n m.n≤m∧m<length(u)⊃member(nth(u,m),nthcdr(u,n))| (open lesseq member)
(use normal mode: always)(use * nthcdr_car_cdr mode: exact))
;∀U N M.N≤M∧M<LENGTH U⊃MEMBER(NTH(U,M),NTHCDR(U,N))
;13
;trivial_nthcdr
(ue (phi3 |λu n.length(u)≤n⊃nthcdr(u,n)=nil|) doubleinduction1
(part 1#1 (open lesseq)))
(label trivial_nthcdr)
;14
;allp_nthcdr
(ue (phi3 |λu n.allp(a,u)⊃allp(a,nthcdr(u,n))|) doubleinduction1 (open allp))
;∀U N.ALLP(A,U)⊃ALLP(A,NTHCDR(U,N))
(label allp_nthcdr)
;15
;nth nthcdr
(ue (phi3 |λu n.n<length u∧m<length(nthcdr(u,n))⊃nth(nthcdr(u,n),m)=nth(u,m+n)|)
doubleinduction1 )
;∀U N.N<LENGTH U∧M<LENGTH (NTHCDR(U,N))⊃NTH(NTHCDR(U,N),M)=NTH(U,M+N)
;16
;length nthcdr
(ue (phi3 |λu n.n≤length u⊃length(nthcdr(u,n))=length u-n|) doubleinduction1
(use successor_minus mode: always) (open minus)(part 1#1#1 (open lesseq)))
;∀U N.N≤LENGTH U⊃LENGTH (NTHCDR(U,N))=LENGTH U-N
;nthcdr_induction1 and nthcdr_induction
(proof nthcdr_induction)
(assume |∀n.n<length(u)∧phi4(nthcdr(u,n'),n')⊃phi4(nth(u,n).nthcdr(u,n'),n)|)
(label n_i_1)
(derive |∀n.n<length(u)⊃(phi4(nthcdr(u,n'),n')⊃phi4(nthcdr(u,n),n))| *
(use nthcdr_car_cdr mode: always))
(label n_i_2)
; two cases
(derive |length(u)≤n∨n<length(u)| trichotomy2)
(label n_i_cases)
;one completely trivial
(assume |length(u)≤n|)
(label n_i_c1)
(trw |length(u)-n=0⊃
(phi4(nthcdr(u,length(u)-n),length(u)-n)⊃
phi4(nthcdr(u,length(u)-n'),length(u)-n'))|(open minus pred) )
(label n_i_3)
(derive |phi4(nthcdr(u,length(u)-n),length(u)-n)⊃
phi4(nthcdr(u,length(u)-n'),length(u)-n')|
(n_i_c1 total_subtraction n_i_3 ))
(label n_i_case1)
;the other quite trivial too...
(assume |n<length(u)|)
(label n_i_c2)
(ue (n |length(u)-(n')|) n_i_2 )
;LENGTH U-N'<LENGTH U⊃
;(PHI4(NTHCDR(U,(LENGTH U-N')'),(LENGTH U-N')')⊃
; PHI4(NTHCDR(U,LENGTH U-N'),LENGTH U-N'))
(rw * (use n_i_c2)(use minusfact11 ue: ((n.|length(u)|)) )
(use minusfact10 mode: exact direction: reverse))
;PHI4(NTHCDR(U,LENGTH U-N),LENGTH U-N)⊃PHI4(NTHCDR(U,LENGTH U-N'),LENGTH U-N')
(label n_i_case2)
(cases n_i_cases n_i_case1 n_i_case2)
;PHI4(NTHCDR(U,LENGTH U-N),LENGTH U-N)⊃PHI4(NTHCDR(U,LENGTH U-N'),LENGTH U-N')
(ue (a |λn.phi4(nthcdr(u,length(u)-n),length(u)-n)|) proof_by_induction *
(part 1(use last_nthcdr mode: exact)(open minus)) )
(label n_i_5)
;PHI4(NIL,LENGTH U)⊃(∀N.PHI4(NTHCDR(U,LENGTH U-N),LENGTH U-N))
(assume |phi4(nil,length(u))|)(label n_i_6)
(derive |∀N.PHI4(NTHCDR(U,LENGTH U-N),LENGTH U-N)| (n_i_5 n_i_6))
(ue (n |length u|) * )
;PHI4(U,0)
;this gives nthcdr_induction1
(ci (n_i_6 n_i_1))
;PHI4(NIL,LENGTH U)∧
;(∀N.N<LENGTH U∧PHI4(NTHCDR(U,N'),N')⊃PHI4(NTH(U,N).NTHCDR(U,N'),N))⊃PHI4(U,0)
;nthcdr_induction follows
(ue ((phi4.|λu n.phi(u)∧n=n|)(u.u)) *)
;PHI(NIL)∧(∀N.N<LENGTH U∧PHI(NTHCDR(U,N'))⊃PHI(NTH(U,N).NTHCDR(U,N')))⊃PHI(U)
;The principle of nthcdr induction is a trick to reduce induction on lists to finite
;induction on numbers. Assume a list U is given; we can prove that U has a certain
;property PHI from the fact that the null list has property PHI and that if X.V is
;a tail of U and V has the property PHI then X.V has the property PHI.
;However, using the functions NTH and NTHCDR we can formulate this method of proof
;as finite descent from PHI(NTHCDR(U,LENGTH(U))) to PHI(NTHCDR(U,0)).
;Indeed we prove by induction on N
;∀N.PHI(NTHCDR(U,LENGTH(U)-N)).
;For N=0, NTHCDR(U,LENGTH(U)-N) is NIL, and we have PHI(NIL).
;Assume PHI(NTHCDR(U,LENGTH(U)-N)). If N≥LENGTH(U) since subtraction is defined
;as a total function on nonnegative integers we have
;LENGTH(U)-N = 0 = LENGTH(U)-N'
;so the induction step is trivial. If N<LENGTH(U),
;LENGTH(U)-N=(LENGTH(U)-N')' by elementary arithmetic
;and
;∀K.K<LENGTH(U)⊃ ( NTHCDR(U,K') ⊃ NTHCDR(U,K))
;is the inductive step of our principle, so we can complete the induction step,
;by letting K to be LENGTH(U)-N' :
;NTHCDR(U,LENGTH(U)-N) ⊃ NTHCDR(U,LENGTH(U)-N')
;Finally it is convenient to write
;NTHCDR(U,K) as NTH(U,K).NTHCDR(U,K') (using NTHCDR_CAR_CDR)
;nthcdr_induction1 is a slight generalization, with an extra inductive variable
;facts about fstposition
(wipe-out)
(get-proofs nth prf ekl sys)
(proof fstpositionprop)
(trw |∀k.¬null k'|)
(label simpinfo)
(unlabel simpinfo posfacts sortpos)
(ue (phi |λu.(null fstposition(u,y)⊃¬member(y,u))∧
(member(y,u)⊃natnum fstposition(u,y))∧
(null fstposition(u,y)∨natnum fstposition(u,y))|) listinduction
(part 1 (open member fstposition) (use normal mode: always)))
;∀U.(NULL FSTPOSITION(U,Y)⊃¬MEMBER(Y,U))∧
; (MEMBER(Y,U)⊃NATNUM(FSTPOSITION(U,Y)))∧
; (NULL FSTPOSITION(U,Y)∨NATNUM(FSTPOSITION(U,Y)))
(label simpinfo posfacts)
(unlabel simpinfo sortpos)
(ue (phi |λu.∀y.sexp fstposition(u,y)|) listinduction
(part 1 (open member fstposition) (use normal mode: always)))
;∀U Y.SEXP FSTPOSITION(U,Y)
(label simpinfo sortpos)
;pos_length
(ue (phi |λu.∀y.member(y,u)⊃fstposition(u,y)<length(u)|) listinduction
(part 1 (open member fstposition) (use normal mode: always)))
;∀U Y.MEMBER(Y,U)⊃FSTPOSITION(U,Y)<LENGTH U
;lemmata nth_fstposition and fstposition_nth
;lemma nth_fstposition
(ue (phi |λu.∀n.member(n,u)⊃nth(u,fstposition(u,n))=n|) listinduction
(use normal mode: always)
(open member fstposition nth))
;∀U N.MEMBER(N,U)⊃NTH(U,FSTPOSITION(U,N))=N
(label nth_fstposition)
(proof fstposition_nth)
1. (ue (phi |λu.0<length u⊃fstposition(u,nth(u,0))=0|)
listinduction (open fstposition nth member))
;∀U.0<LENGTH U⊃FSTPOSITION(U,CAR U)=0
2. (derive |n<length u ∧ x=nth(u,n) ⊃ member(x,u)| (nthmember))
3. (derive |uniqueness(x.u)∧n<length u⊃¬x=nth(u,n)| * (open uniqueness))
4. (ue (phi3 |λu n.uniqueness u∧n<length u⊃fstposition(u,nth(u,n))=n|)
doubleinduction1 *
(open fstposition nth member uniqueness) -3 nthmember)
;∀U N.UNIQUENESS(U)∧N<LENGTH U⊃FSTPOSITION(U,NTH(U,N))=N
;equivalence of uniqueness and inj
(wipe-out)
(get-proofs nth prf ekl sys)
(proof uniqueness_inj)
(ue (phi3 |λu n.uniqueness u⊃uniqueness nthcdr(u,n)|) doubleinduction1
(open uniqueness nthcdr))
;∀U N.UNIQUENESS(U)⊃UNIQUENESS(NTHCDR(U,N))
(label uniqueness_nthcdr)
(assume |uniqueness(u)|)
(label ui1)
(assume |i<length u|)
(label ui2)
(assume |j<length u|)
(label ui3)
(assume |nth(u,i)=nth(u,j)|)
(label ui4)
(derive |uniqueness(nthcdr(u,i))|(uniqueness_nthcdr ui1))
(rw * (use nthcdr_car_cdr ui2 mode: always) (open uniqueness))
;¬MEMBER(NTH(U,I),NTHCDR(U,I'))∧UNIQUENESS(NTHCDR(U,I'))
;deps: (UI1 UI2)
;labels: NTH_IN_NTHCDR
;∀U N M.N≤M∧M<LENGTH U⊃MEMBER(NTH(U,M),NTHCDR(U,N))
(ue ((u.u)(n.|i'|)(m.j)) nth_in_nthcdr
(use ui4 mode: exact direction: reverse)
(use ui3 * mode: exact))
;¬I'≤J
;deps: (UI1 UI2 UI3 UI4)
;labels: LESS_LESSEQSUCC
;∀M N.M<N=M'≤N
(ue ((m.i)(n.j)) less_lesseqsucc *)
;¬I<J
(label ui_way1)
;deps: (UI1 UI2 UI3 UI4)
(ci (ui1 ui2 ui3 ui4))
;UNIQUENESS(U)∧I<LENGTH U∧J<LENGTH U∧NTH(U,I)=NTH(U,J)⊃¬I<J
(ue ((i.j)(j.i)) *)
;UNIQUENESS(U)∧J<LENGTH U∧I<LENGTH U∧NTH(U,J)=NTH(U,I)⊃¬J<I
(derive |¬j<i| (* ui1 ui2 ui3 ui4))
(label ui_way2)
;deps: (UI1 UI2 UI3 UI4)
(derive |i=j| (trichotomy ui_way1 ui_way2))
;deps: (UI1 UI2 UI3 UI4)
(ci (ui1 ui2 ui3 ui4))
;UNIQUENESS(U)∧I<LENGTH U∧J<LENGTH U∧NTH(U,I)=NTH(U,J)⊃I=J
(trw |uniqueness(u)⊃inj(u)| * (open inj))
;UNIQUENESS(U)⊃INJ(U)
;equivalence of uniqueness and inj
(proof inj_uniqueness)
(assume |inj u|)(label iu1)
(rw * (open inj))
;∀N M.N<LENGTH U∧M<LENGTH U∧NTH(U,N)=NTH(U,M)⊃N=M
(label iu2)
(assume |member(nth(u,n),nthcdr(u,n'))|)(label iu3)
(assume |length(u)≤n'|)(label iu4)
(rw iu3 (use trivial_nthcdr iu4 mode: always) (open member))
;FALSE
;deps: (IU3 iu4)
(ci iu4)
;¬LENGTH U≤N'
;deps: (IU3)
(derive |n'<length u| (* trichotomy2))
(label iu6)
;we use:
;labels: MEMBER_NTH
;∀U Y.MEMBER(Y,U)⊃(∃N.N<LENGTH U∧NTH(U,N)=Y)
(ue ((u.|nthcdr(u,n')|)(y.|nth(u,n)|)) member_nth iu3)
;∃N1.N1<LENGTH (NTHCDR(U,N'))∧NTH(NTHCDR(U,N'),N1)=NTH(U,N)
(label iu7)
(define mv |mv<length(nthcdr(u,n'))∧nth(nthcdr(u,n'),mv)=nth(u,n)| *)
(label iu8)
;we use:
;labels: NTH_NTHCDR
;∀U N M.N<LENGTH U∧M<LENGTH (NTHCDR(U,N))⊃
; NTH(NTHCDR(U,N),M)=NTH(U,M+N)
(ue ((u.u)(n.|n'|)(m.mv)) nth_nthcdr (iu8 iu6))
;NTH(U,N)=NTH(U,(MV+N)')
(label iu9)
(ue ((u.u)(n.|n'|)) length_nthcdr iu6 (open lesseq))
;LENGTH (NTHCDR(U,N'))=LENGTH U-N'
(derive |mv<length u-n'| (iu8 *))
(ue ((n.|length u|)(k.|n'|)(m.mv)) inequality_law * iu6)
;(MV+N)'<LENGTH U
(label iu10)
(derive |n=(mv+n)'| (iu2 iu6 succ_less_less iu9 iu10))
(ue (a |λn.n≠m+n'|) proof_by_induction)
;∀N.¬N=(M+N)'
(rw -2 *)
;FALSE
;deps: (IU1 IU3)
(ci iu3)
;¬MEMBER(NTH(U,N),NTHCDR(U,N'))
;deps: (IU1)
(ue ((phi.|λu.uniqueness u|)(u.u)) nthcdr_induction (open uniqueness) *)
;UNIQUENESS(U)
;deps: (IU1)
(ci IU1)
;INJ(U)⊃UNIQUENESS(U)
;proof of facts about sets
(wipe-out)
(get-proofs nth prf ekl sys)
(proof setfacts)
;nth_allp
(assume |∀n.n<length(u)⊃phi1(nth(u,n))|)
(label allp_intr1)
(ue ((phi.|λu.allp(phi1,u)|)(u.u)) nthcdr_induction
(open allp) (use * mode: always))
;ALLP(PHI1,U)
(ci allp_intr1)
;(∀N.N<LENGTH U⊃PHI1(NTH(U,N)))⊃ALLP(PHI1,U)
;mklset_fact
;the set of members of a list can be expressed in terms of nth
(derive |∀x.(mklset(u))(x)≡(∃k.k<length u∧nth(u,k)=x)|
(nthmember member_nth) (open mklset))
(ue ((av.|mklset(u)|)(bv.|λx.(∃k.k<length u∧nth(u,k)=x)|)) set_extensionality
* (open epsilon) )
;MKLSET(U)=(λX.(∃K.K<LENGTH U∧NTH(U,K)=X))